Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    leq(0,y)  → true
2:    leq(s(x),0)  → false
3:    leq(s(x),s(y))  → leq(x,y)
4:    if(true,x,y)  → x
5:    if(false,x,y)  → y
6:    x - 0  → x
7:    s(x) - s(y)  → x - y
8:    mod(0,y)  → 0
9:    mod(s(x),0)  → 0
10:    mod(s(x),s(y))  → if(leq(y,x),mod(s(x) - s(y),s(y)),s(x))
There are 6 dependency pairs:
11:    LEQ(s(x),s(y))  → LEQ(x,y)
12:    s(x) -# s(y)  → x -# y
13:    MOD(s(x),s(y))  → IF(leq(y,x),mod(s(x) - s(y),s(y)),s(x))
14:    MOD(s(x),s(y))  → LEQ(y,x)
15:    MOD(s(x),s(y))  → MOD(s(x) - s(y),s(y))
16:    MOD(s(x),s(y))  → s(x) -# s(y)
The approximated dependency graph contains 3 SCCs: {12}, {11} and {15}.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006